| Definitions | x:A  B(x),  b, ES, Type, IdLnk, Atom$n, Id, a:A fp B(a), x:A B(x),  e@i. P(e), s = t, if b then t else f fi , t  T, t.1, E, (e < e'), e c e', x,y:A//B(x;y),  , x:A. B(x), vartype(i;x), Top, f(x)?z, IdDeq,  x.A(x),  x. t(x), P   Q, @i discrete ds, <a, b>,  , {T}, SQType(T), State(ds),  , {x:A| B(x)} , Knd, valtype(e), P & Q, A c B, state@i, (state after e)+t, f(a), left + right, Unit, False, True, case b of inl(x) => s(x) | inr(y) => t(y),  ,   , A  B, EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), x,y. t(x;y),  A, isrcv(e), sender(e), let x,y = A in B(x;y), e loc e' , (e <loc e'), P  Q, EqDecider(T), EOrderAxioms(E; pred?; info), EState(T), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r s, constant_function(f;A;B),  x:A. B(x), loc(e), rcv(l,tg), kind(e), locl(a), source(l), s ~ t, P  Q, P Q, val(e), (state when e), weak-precond-send-p(es;T;A;l;tg;a;ds;P;f) |
f:({s:State(ds)|